/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package semantics.reachability;

import java.util.Collections;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Set;
import java.util.Stack;
import semantics.State;
import semantics.TIOARuntime;
import syntax.Domain;
import syntax.TIOA;
import syntax.Transition;
import util.TaggedWeightedObject;

/**
 *
 * @author ennouaary
 */
public class ExhaustiveReachabilityAnalysis implements ReachabilityAnalysis{

    Stack<State> states;
    Set<State> handledStates;
    
    @Override
    public TIOARuntime analyse(TIOA tioa) {
        Float timeStep = 0F;
        Float minDelay = 0F, maxDelay = 0.F;
        State newState;
        State currentState;
        TIOARuntime tioaRuntime = new TIOARuntime(tioa);
        //Initialise initial state:
        //current state = l0 && v_x <- 0 for each x
        states = new Stack<State>();
        handledStates = new HashSet<State>();
        currentState = State.initializeState(tioa);
        states.push(currentState);

        while (!states.empty()) {
            currentState = states.pop();
            handledStates.add(currentState);
            //float outputDelay = Parameters.getInfinity();
            List<Transition> unreacheableOutputTrans = new LinkedList<Transition>();
            List<Transition> potTrans = new LinkedList<Transition>();
            Domain bestExecRange = Domain.getInfinityUnreachableDomain();
            Domain currRange;

            //TreeMap<Domain, Transition> transTree = new TreeMap<>(domainComparator);
            List<TaggedWeightedObject> minTransitions = new LinkedList<TaggedWeightedObject>();
            List<TaggedWeightedObject> maxTransitions = new LinkedList<TaggedWeightedObject>();
            TaggedWeightedObject wo;
            for (Transition transition : currentState.getLocation().getOutgoingTrans()) {
                if (transition.getMessage().isOutput()) {
                    minDelay = currentState.minDelay(transition);
                    maxDelay = currentState.maxDelay(transition);
                    wo = new TaggedWeightedObject(TaggedWeightedObject.TAG.MIN, minDelay, transition);
                    minTransitions.add(wo);
                    wo = new TaggedWeightedObject(TaggedWeightedObject.TAG.MAX, maxDelay, transition);
                    maxTransitions.add(wo);
                }
                else {
                    potTrans.add(transition);
                }                                                
            }
            List<TaggedWeightedObject> toHandleTrans = new LinkedList<TaggedWeightedObject>();
            toHandleTrans.addAll(minTransitions);
            toHandleTrans.addAll(maxTransitions);
            
            Collections.sort(toHandleTrans);
            Iterator<TaggedWeightedObject> iter = toHandleTrans.listIterator();
            while (iter.hasNext()) {
                wo = iter.next();
                if (wo.getTag() == TaggedWeightedObject.TAG.MAX) {
                    break;
                } else {
                    potTrans.add((Transition)wo.getObject());
                }                
            }
            while (iter.hasNext()) {
                wo = iter.next();
                if (wo.getTag() == TaggedWeightedObject.TAG.MIN) {
                    unreacheableOutputTrans.add((Transition)wo.getObject());
                }               
            }
                        
            for (Transition transition : unreacheableOutputTrans) {
                tioaRuntime.putTransitionReachability(transition, false);
//                transition.setReachable(false);
            }

            for (Transition transition : potTrans) {                
                if (currentState.isExecutable(transition)) {
                    tioaRuntime.putLocationReachability(transition.getDestLocation(), true);
                    tioaRuntime.putTransitionReachability(transition, true);
//                    transition.setReachable(true);
                    tioaRuntime.putTransitionNewAddedState(transition, currentState);
                    //transition.addLastStateToPool(currentState);
                    newState = currentState.computeNewState(transition);
                    if (!handledStates.contains(newState)) {
//                        transition.getDestLocation().setReachable(true);
                        states.push(newState);
                    }
                }
//                timeStep = currentState.minDelay(transition);
//                //if v+delta \models G time guard 
//                newState = computeNewStateWithoutReset(currentState, transition, timeStep);
//                if (newState.isModel(transition.getClockGuard())) {
//                    transition.setReachable(true);
//                    applyReset(newState, transition);
//                    if (!handledStates.contains(newState)) {
//                        transition.getDestLocation().setReachable(true);
//                        states.push(newState);
//                    }
//                }
            }

        }
        return tioaRuntime;
        
    }
    
}
